(set-logic ALL)
(set-info :status sat)
(declare-datatypes ((list 0)) (((cons (tail list)) (nil))))
(declare-fun P (Int) Bool)
(declare-fun S () (Set list))
(declare-fun l () list)
(assert ((_ is cons) l))
(assert (set.member l S))
(assert (set.member nil S))
(assert (not (P 0)))
(check-sat)
